Nuprl Lemma : isl_wf
11,40
postcript
pdf
A
,
B
:Type,
x
:(
A
+
B
). isl(
x
)
latex
Definitions
isl(
x
)
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
bfalse
wf
,
btrue
wf
origin
A,B:Type, x:(A + B). isl(x) 
A,B:Type, x:(A + B). isl(x) Tx:A. B(x)